//  IDVI 1.0 source copyright 1996 Garth A. Dickie
//
//  This source is free for non-commercial use.  No warranty, etc.
//  Please acknowledge reuse by including the line:
//
//  "Based in part on IDVI 1.0 source copyright 1996 Garth A. Dickie"
//
//  in your documentation and source code.  For commercial use or
//  distribution, please contact the author.  Please also send
//  questions, comments, bug reports, or fixes.
//
//  Best Regards,
//  Garth A. Dickie
//  dickie@elastic.avid.com

package ibook.v10.idvi.split;

import java.io.*;
import java.net.*;
import java.util.*;

import ibook.v10.colors.Colors;
import ibook.v10.idvi.IDVI;
import ibook.v10.idvi.MessageContext;
import ibook.v10.idvi.dvi.*;
import ibook.v10.idvi.font.DVIFont;
import ibook.v10.idvi.io.*;
import ibook.v10.parameter.*;

// The clause 'implements DVIFormat' lets us refer to the constants
// defined in that interface as though they were defined in this class.

public class Splitter extends DVIDocument implements DVIFormat {
    final private static String     kDefaultCode = "ibook.release.DVIOnePageApplet";
    final private static String     kDocumentSuffix = ".dvi";
    final private static String     kImageInfoName = "idvi.images";
    final private static String     kImageSuffix = ".gif";
    final private static String     kFontInfoName = "idvi.fonts";

    private ParameterProcessor  parameter;
    private MessageContext  context;

    private String      documentName;
    private URL         documentURL;

    private int         dpi             = IDVI.kDefaultDPI;
    private int         scaleMin        = IDVI.kDefaultScaleMin;
    private int         scaleMax        = IDVI.kDefaultScaleMax;
    private int         scaleDefault    = IDVI.kDefaultScaleDefault;
    private String      scalePrefix     = IDVI.kDefaultScalePrefix;
    private int         pageFirst       = IDVI.kDefaultPageMin;
    private int         pageDefault     = IDVI.kDefaultPageMin;
    private String      pagePrefix      = IDVI.kDefaultPagePrefix;
    private String      prefix          = "";
    private String      index           = IDVI.kDefaultIndex;
    private boolean     centered        = IDVI.kDefaultCentered;
    private int         centerPage;
    private Hashtable   translate;

    private String      template;

    private int         backgroundColor     = IDVI.kDefaultBackgroundColor;
    private int         foregroundColor     = IDVI.kDefaultForegroundColor;
    private int         selectionColor      = IDVI.kDefaultSelectionColor;
    private int         linkColor           = IDVI.kDefaultLinkColor;
    private int         selectedLinkColor   = IDVI.kDefaultSelectedLinkColor;

    private int         defaultPageDefault;
    private int         defaultScaleMax;
    private int         defaultScaleDefault;
    private String      defaultIndex;
    private int         pageMax;

    private Vector      pageVector      = new Vector( );
    private Hashtable   specialMap      = new Hashtable( );
    private Vector      psFileVector    = new Vector( );
    private byte[ ]     postamble       = new byte[ kPostambleLength ];


    // The constuctor reads the command-line parameters, at the moment.
    // This will have to change when we are able to take parameters from
    // the dvi file or from an html template file.  In that case, we should
    // read the minimal number of parameters here (documentName, fontSource,
    // dpi), then read the dvi file and template file, then read the rest
    // of the parameters, allowing that they may come from the dvi file.
    //
    // This also means that we have to postpone thinking about the href
    // translation until after we have read the whole dvi file and template,
    // since these might contain a definition for pageFirst.

    public Splitter( ParameterProcessor parameter, MessageContext context )
            throws ParameterException, IOException {

        this.parameter = parameter;
        this.context = context;

        // The order here matters, since the parameter.get... methods may
        // throw exceptions, which fall through to our parent.  If there
        // is no document name on the command line, we want to print usage
        // information without checking for any other parameters.  Then
        // we get the other required parameter, fontSource; if this is missing,
        // an error message is printed before the usage information.  Then
        // we get the remaining parameters; any format errors in these parameters
        // will be reported without printing the whole usage message.

        documentName     = parameter.getString   ( ""             );

        if( documentName.length( ) <= kDocumentSuffix.length( ) ||
                ! documentName.endsWith( kDocumentSuffix )) {

            documentName += kDocumentSuffix;
        }

        setFontBase(       parameter.getFileURL  ( "fontSource"   ));
        setTemplateFile(   parameter.getString   ( "templateFile" ));

        dpi              = parameter.getInteger  ( "dpi"         , dpi );
        scaleMin         = parameter.getInteger  ( "scaleMin"    , IDVI.kScaleMin, IDVI.kScaleMax, scaleMin );

        defaultScaleMax = Math.max( scaleMax, scaleMin );
        scaleMax         = parameter.getInteger  ( "scaleMax"    , scaleMin, IDVI.kScaleMax, defaultScaleMax);

        defaultScaleDefault = Math.max( Math.min( scaleDefault, scaleMax ), scaleMin );
        scaleDefault     = parameter.getInteger  ( "scaleDefault", scaleMin, scaleMax, defaultScaleDefault );

        pageFirst        = parameter.getInteger  ( "pageFirst"   , pageFirst );

        defaultPageDefault = pageFirst;
        pageDefault      = parameter.getInteger  ( "pageDefault" , pageFirst, pageFirst - 1, pageFirst );

        prefix           = parameter.getString   ( "prefix"      , prefix );
        scalePrefix      = parameter.getString   ( "scalePrefix" , scalePrefix );

        pagePrefix       = parameter.getString   ( "pagePrefix"  , pagePrefix );
        pagePrefix = prefix + pagePrefix;

        defaultIndex = ParameterProcessor.guessIndex( prefix, index );
        index            = parameter.getString   ( "index"       , defaultIndex );

        centered         = parameter.getBoolean  ( "centered"    , centered );
        centerPage       = parameter.getInteger  ( "centerPage"  , pageFirst - 1 );
        translate        = parameter.getHashtable( "translate"   , translate );

        backgroundColor   = parameter.getColor( "backgroundColor"  , backgroundColor );
        foregroundColor   = parameter.getColor( "foregroundColor"  , foregroundColor );
        selectionColor    = parameter.getColor( "selectionColor"   , selectionColor );
        linkColor         = parameter.getColor( "linkColor"        , linkColor );
        selectedLinkColor = parameter.getColor( "selectedLinkColor", selectedLinkColor );

        setDPI( dpi );

        if( scalePrefix.length( ) == 0 )
            throw new ParameterValueException( "scalePrefix", "", "string (must be non-empty)" );
    }

    private void setTemplateFile( String templateFileName )
            throws IOException {
        
        RandomAccessFile file = new RandomAccessFile( templateFileName, "r" );

        byte[ ] bytes = new byte[ ( int ) file.length( ) ];
        file.readFully( bytes );
        file.close( );

        template = new String( bytes, 0 );
    }

    private void checkLength( ) {
//      context.showMessage( "source file \"" + documentName + "\" has length = " + new File( documentName ).length( ));
    }




    public void readDVI( ) throws DVIFormatException, IOException, ParameterValueException {
        checkLength( );

        DVIInputStream source = new DVIInputStream( openDVIInputStream( ));

        try {
            parseHeader( source );

            DVITokenizer tokenizer = new DVITokenizer( source, this, context );

            int pageNumber = 0;
            while( tokenizer.token == DVITokenizer.kTokenBeginPage ) {
                context.showMessage( "Reading page " + ( pageNumber + pageFirst ));
                pageVector.addElement( new PageInfo(
                    tokenizer, scaleMin, scaleMax, getDVIName( pageNumber + pageFirst ), specialMap, psFileVector ));
                pageNumber ++;
            }

            if( pageVector.size( ) == 0 )
                throw new DVIFormatException( "DVI File % contains 0 pages!" );

            source.read( postamble );

            pageMax = pageFirst + pageVector.size( ) - 1;
            pageDefault = Math.min( pageDefault, pageMax );

            constructTemplateParameterProcessor( );

        } catch( DVIFormatException e ) {
            throw new DVIFormatException( e, documentName );
        } finally {
            source.close( );
        }
    }

    void writeDVI( ) throws DVIFormatException, IOException, MalformedURLException {
        checkLength( );

        DVIInputStream source = new DVIInputStream( openDVIInputStream( ));
        Hashtable font = new Hashtable( );
        
        checkLength( );

        try {
            byte[ ] header = new byte[ kHeaderLength ];
            source.read( header );

            source.skip( source.unsigned1( ));

            int pageNumber = 0;
            while( source.unsigned1( ) == kCommandBOP ) {
                DVIOutputStream dest =
                    new DVIOutputStream( openDVIOutputStream( pageFirst + pageNumber ));

                try {
                    dest.write( header );

                    String comment = "dvisplit output, page " + ( pageFirst + pageNumber );
                    dest.write( comment.length( ));
                    dest.write( comment );

                    int page1Offset = dest.getOffset( );

                    dest.write( kCommandBOP );
                    dest.write( source, kPageHeaderLength - 4 );
                    source.unsigned4( );
                    dest.write4( kMagicFirstBackpointer );

                    Hashtable usedFont = new Hashtable( );
                    PageInfo pageInfo = ( PageInfo ) pageVector.elementAt( pageNumber );
                    writePage( source, dest, pageInfo.pageSpecialMap, font, usedFont );

                    int postOffset = dest.getOffset( );

                    dest.write( kCommandPOST );
                    dest.write4( page1Offset ); // offset in file of last page
                    dest.write( postamble, 4, kPostambleLength - 6 );
                    dest.write2( 1 );           // number of pages

                    Enumeration keyEnumeration = usedFont.keys( );
                    Enumeration fontEnumeration = usedFont.elements( );

                    while( keyEnumeration.hasMoreElements( )) {
                        dest.writeVariableSized(
                            kCommandFNTDEF1,
                            (( Integer ) keyEnumeration.nextElement( )).intValue( ));
                        
                        dest.write(( byte[ ] ) fontEnumeration.nextElement( ));
                    }

                    dest.write( kCommandPOSTPOST );
                    dest.write4( postOffset );
                    dest.write( kMagicVersion );
                    dest.write( kMagicFiller );
                    dest.write( kMagicFiller );
                    dest.write( kMagicFiller );
                    dest.write( kMagicFiller );
                } finally {
                    dest.close( );
                }
                
                ++ pageNumber;
            }
        } finally {
            source.close( );
        }
    }

    public void writeHTML( ) throws IOException {
        int scaleCount = scaleMax - scaleMin + 1;

        for( int scaleIndex = 0; scaleIndex < scaleCount; ++ scaleIndex ) {
            int scale = scaleIndex + scaleMin;

            computedParameterHashtable.put( "scale", Integer.toString( scale ));

            int top   = Integer.MAX_VALUE;
            int left  = Integer.MAX_VALUE;
            int right = Integer.MIN_VALUE;

            Enumeration pages = pageVector.elements( );
            while( pages.hasMoreElements( )) {
                PageInfo info = ( PageInfo ) pages.nextElement( );

                if( info.pageTop  [ scaleIndex ] < top   ) top   = info.pageTop  [ scaleIndex ];
                if( info.pageLeft [ scaleIndex ] < left  ) left  = info.pageLeft [ scaleIndex ];
                if( info.pageRight[ scaleIndex ] > right ) right = info.pageRight[ scaleIndex ];
            }

            if( centered && centerPage >= pageFirst ) {
                PageInfo centerInfo = ( PageInfo ) pageVector.elementAt( centerPage - pageFirst );

                int center = ( centerInfo.pageLeft[ scaleIndex ] + centerInfo.pageRight[ scaleIndex ] ) / 2;
                int halfWidth = Math.max( right - center, center - left );

                left = center - halfWidth;
                right = center + halfWidth;
            }

            int scaledTop   = top / scale;
            int scaledLeft  = left / scale;
            int scaledRight = ( right  + scale - 1 ) / scale;
            int scaledWidth = scaledRight  - scaledLeft;

            int pageNumber = pageFirst;
            pages = pageVector.elements( );
            while( pages.hasMoreElements( )) {
                PageInfo info = ( PageInfo ) pages.nextElement( );

                int pageScaledLeft = scaledLeft;
                int pageScaledWidth = scaledWidth;

                if( centered ) {
                    int spaceLeft = info.pageLeft[ scaleIndex ] / scale - scaledLeft;
                    int spaceRight = scaledRight - ( info.pageRight[ scaleIndex ] + scale - 1 ) / scale;
                    int space = Math.min( spaceLeft, spaceRight );
                    
                    pageScaledLeft = scaledLeft + space;
                    int pageScaledRight = scaledRight - space;
                    pageScaledWidth = pageScaledRight - pageScaledLeft;
                }

                int pageScaledTop = scaledTop;
                int pageScaledBottom = ( info.pageBottom[ scaleIndex ] + info.expansion[ scaleIndex ] + scale - 1 ) / scale;
                int pageScaledHeight = pageScaledBottom - pageScaledTop;

                computedParameterHashtable.put( "page"           , Integer.toString(   pageNumber       ));
                computedParameterHashtable.put( "width"          , Integer.toString(   pageScaledWidth  ));
                computedParameterHashtable.put( "height"         , Integer.toString(   pageScaledHeight ));
                computedParameterHashtable.put( "leftmargindelta", Integer.toString( - pageScaledLeft   ));
                computedParameterHashtable.put( "topmargindelta" , Integer.toString( - pageScaledTop    ));

                PrintStream output = openHTMLPrintStream( pageNumber, scale );
                try {
                    output.print( templateParameterStub.expandString( template ));
                } finally {
                    output.close( );
                }

                ++ pageNumber;
            }
        }
    }

    public void writeImages( )
            throws IOException {

        int scaleCount = scaleMax - scaleMin + 1;
        int scaleIndexInitial = scaleMin == 1 ? 1 : 0;

        try {
            Enumeration psFileEnumeration = psFileVector.elements( );
            while( psFileEnumeration.hasMoreElements( )) {
                PSFileInfo info = ( PSFileInfo ) psFileEnumeration.nextElement( );

                String psFileName;
                try {
                    psFileName = info.parameter.getString( "psfile" );
                } catch( ParameterMissingException e ) {
                    throw new Error( "internal error: psfile missing in psfile special." );
                }
                long psFileModified = new File( psFileName ).lastModified( );

                writeImageHeader( psFileName, info );
                writeImageInfo( psFileName, psFileModified, info, 1 );
                for( int scaleIndex = scaleIndexInitial; scaleIndex < scaleCount; ++ scaleIndex )
                    writeImageInfo( psFileName, psFileModified, info, scaleIndex + scaleMin );
            }
        } finally {
            closeImageInfo( );
        }
    }

    public void listFonts( )
            throws IOException {

        PrintStream fontInfo = openPrintStream( kFontInfoName );

        try {
            Enumeration fonts = getFonts( );

            while( fonts.hasMoreElements( )) {
                DVIDocumentFont documentFont = ( DVIDocumentFont ) fonts.nextElement( );
                DVIFont font = documentFont.getFont( );

                if( font != null ) {
                    fontInfo.print( "font " );
                    fontInfo.println( font.getName( ));
                }
            }
        } finally {
            fontInfo.close( );
        }
    }




    // Routines to manage the parameter processor which is used to expand HTML
    // template files.  This parameter processor uses ParameterUnionStub
    // to implement the following priority scheme:
    //
    //  1. ComputedParameters       Parameters such as scale, page, width, height.
    //  2. Parameters               Command-line parameters of the form -a b
    //  3. DVIParameters            idvi:name=value specials in the dvi file (not implemented)
    //  4. TemplateParameters       a=b lines at the head of the HTML template file (not implemented)
    //  5. DefaultParameters        Defaults from the interface HTMLParameters
    //  6. Environment              The command-line environment (disabled at the moment)

    private ParameterProcessor  templateParameterProcessor;
    private ParameterExpandStub templateParameterStub;

    private Hashtable           dviParameterHashtable = new Hashtable( );
    private Hashtable           templateParameterHashtable = new Hashtable( );
    private Hashtable           computedParameterHashtable;

    private void constructTemplateParameterProcessor( ) throws ParameterValueException {
        computedParameterHashtable = constructComputedParameterHashtable( );

        ParameterUnionStub unionStub = new ParameterUnionStub( );

        unionStub.add( new HashtableParameterStub( computedParameterHashtable ));
        unionStub.add( parameter.getStub( ));

        // unionStub.add( new HashtableParameterStub( dviParameterHashtable ));
        // unionStub.add( new HashtableParameterStub( templateParameterHashtable ));

        unionStub.add( new HashtableParameterStub( constructDefaultParameterHashtable( )));

        templateParameterProcessor = new ParameterProcessor( );
        templateParameterStub = new ParameterExpandStub( unionStub, templateParameterProcessor );
        templateParameterProcessor.setStub( templateParameterStub );
    }

    // Build the defaultParameterHashtable.  This is the set of parameters which
    // has been predefined for all templates, and is independent of the DVI file
    // being processed and the command line options.  We start with the environment
    // which has been passed to us, and add definitions from the interface HTMLParameters.

    private Hashtable constructDefaultParameterHashtable( ) throws ParameterValueException {
        Hashtable result = parameter.getHashtable( "environment", "" );

        String[ ] parameters = HTMLParameters.parameters;
        for( int i = 0; i < parameters.length; i += 2 )
            result.put( parameters[ i ].toLowerCase( ), parameters[ i + 1 ] );

        return result;
    }

    // Build the computedParameterHashtable.  This is the set of parameters which
    // are computed from the command-line options and the contents of the DVI file
    // (only pageMax is computed from the DVI file, at the moment).  It also contains
    // overrides for the paramTags which are unneccessary because the parameters they
    // define have their default values.

    private Hashtable constructComputedParameterHashtable( ) {
        Hashtable result = new Hashtable( );

        //  Note that the key in each of the result.put calls is in all lower case.
        //  This is because a case-insensitive search is done on lookup, by first
        //  converting the lookup key to lower case.

        result.put( "dpi"              , Integer.toString( dpi                 ));
        result.put( "scalemin"         , Integer.toString( scaleMin            ));
        result.put( "scalemax"         , Integer.toString( scaleMax            ));
        result.put( "scaledefault"     , Integer.toString( scaleDefault        ));
        result.put( "pagemin"          , Integer.toString( pageFirst           ));
        result.put( "pagemax"          , Integer.toString( pageMax             ));
        result.put( "pagedefault"      , Integer.toString( pageDefault         ));
        result.put( "prefix"           , prefix                                 );
        result.put( "scaleprefix"      , scalePrefix                            );
        result.put( "pageprefix"       , pagePrefix.substring( prefix.length( )));
        result.put( "index"            , index                                  );
        result.put( "centered"         , String.valueOf  ( centered            ));

        result.put( "backgroundcolor"  , Colors.toNetscapeString( backgroundColor   ));
        result.put( "foregroundcolor"  , Colors.toNetscapeString( foregroundColor   ));
        result.put( "selectioncolor"   , Colors.toNetscapeString( selectionColor    ));
        result.put( "linkcolor"        , Colors.toNetscapeString( linkColor         ));
        result.put( "selectedlinkcolor", Colors.toNetscapeString( selectedLinkColor ));

        String codeBase = parameter.getString( "codeBase", null );
        if( codeBase     == null                  ) result.put( "codebaseparam"       , "" );

        String archive = parameter.getString( "archive", null );
        if( archive      == null                  ) result.put( "archiveparam"        , "" );

        if( dpi          == IDVI.kDefaultDPI      ) result.put( "dpiparamtag"         , "" );
        if( pageFirst    == IDVI.kDefaultPageMin  ) result.put( "pageminparamtag"     , "" );
        if( pageDefault  == defaultPageDefault    ) result.put( "pagedefaultparamtag" , "" );
        if( scaleMin     == IDVI.kDefaultScaleMin ) result.put( "scaleminparamtag"    , "" );
        if( scaleMax     == defaultScaleMax       ) result.put( "scalemaxparamtag"    , "" );
        if( scaleDefault == defaultScaleDefault   ) result.put( "scaledefaultparamtag", "" );

        if( prefix     .equals( IDVI.kDefaultPrefix      )) result.put( "prefixparamtag"     , "" );
        if( pagePrefix .equals( IDVI.kDefaultPagePrefix  )) result.put( "pageprefixparamtag" , "" );
        if( scalePrefix.equals( IDVI.kDefaultScalePrefix )) result.put( "scaleprefixparamtag", "" );
        if( index      .equals( defaultIndex             )) result.put( "indexparamtag"      , "" );

        if( backgroundColor   == IDVI.kDefaultBackgroundColor   ) result.put( "backgroundcolorparamtag"  , "" );
        if( foregroundColor   == IDVI.kDefaultForegroundColor   ) result.put( "foregroundcolorparamtag"  , "" );
        if( selectionColor    == IDVI.kDefaultSelectionColor    ) result.put( "selectioncolorparamtag"   , "" );
        if( linkColor         == IDVI.kDefaultLinkColor         ) result.put( "linkcolorparamtag"        , "" );
        if( selectedLinkColor == IDVI.kDefaultSelectedLinkColor ) result.put( "selectedlinkcolorparamtag", "" );

        return result;
    }




    // Helper functions for writeImages:

    private PrintStream     imageInfo = null;

    private void openImageInfo( ) throws IOException {
        imageInfo = openPrintStream( kImageInfoName );
    }

    private void closeImageInfo( ) throws IOException {
        if( imageInfo != null ) {
            imageInfo.println( );
            imageInfo.close( );
            imageInfo = null;
        }
    }

    private void writeImageHeader( String psFileName, PSFileInfo info )
            throws IOException {

        if( imageInfo == null )
            openImageInfo( );
        else
            imageInfo.println( );

        // We allow one postscript unit of slop on all sides of the bounding
        // box, since many (most?) eps files have slightly incorrect bounding
        // boxes.

        int boundingBoxSlop = ( int ) Math.ceil(( double ) dpi / kPSFileDPI );
        int left = boundingBoxSlop;
        int top = boundingBoxSlop + info.height;

        StringBuffer optionsBuffer = new StringBuffer( );
        Enumeration keys = info.parameterHashtable.keys( );
        Enumeration elements = info.parameterHashtable.elements( );
        while( keys.hasMoreElements( )) {
            String key = ( String ) keys.nextElement( );
            String element = ( String ) elements.nextElement( );
            if( ! key.equals( kPSFileName ))
                optionsBuffer.append( element ).append( " @" ).append( key ).append( ' ' );
        }
        String psFileOptions = optionsBuffer.toString( );

        String psString =
            "TeXDict begin 1 /DVImag X " +
            dpi + " dup /Resolution X /VResolution X " +
            left + " " + top + " moveto " +
            "@beginspecial " + psFileOptions + " @setspecial " +
            "(" + psFileName + ") run @endspecial end showpage quit";

        imageInfo.print( "psfile '" );
        imageInfo.print( psString );
        imageInfo.print( "' " );
        imageInfo.print( info.width + 2 * boundingBoxSlop );
        imageInfo.print( " " );
        imageInfo.print( info.height + 2 * boundingBoxSlop );
        imageInfo.print( " '" );
        imageInfo.print( info.prefix );
        imageInfo.print( "' '" );
        imageInfo.print( scalePrefix );
        imageInfo.print( "'" );
    }

    private void writeImageInfo(
            String psFileName, long psFileModified, PSFileInfo info, int scale )
            throws IOException {

        String outputFileName = info.prefix + scalePrefix + scale + kImageSuffix;
        File outputFile = new File( outputFileName );

        if( outputFile.exists( ) && outputFile.lastModified( ) >= psFileModified )
            imageInfo.print( " not" );
        
        imageInfo.print( ' ' );
        imageInfo.print( scale );
    }




    // Write a single page DVI file, copying from the source DVI file.

    private void writePage(
            DVIInputStream source, DVIOutputStream dest,
            Hashtable pageSpecialMap, Hashtable font, Hashtable usedFont )
            throws IOException, DVIFormatException {

        boolean done = false;

        while( ! done ) {
            int command = source.unsigned1( );
            int length;

            if( command <= kHighCharacter ) {
                dest.write( command );
            } else if( command >= kLowFont && command <= kHighFont ) {
                writeFontSelect( command - kLowFont, dest, font, usedFont );
            } else switch( command ) {
                case kCommandEOP:
                    dest.write( command );
                    done = true;
                    break;

                case kCommandNOP:
                case kCommandPUSH:
                case kCommandPOP:
                case kCommandW0:
                case kCommandX0:
                case kCommandY0:
                case kCommandZ0:
                    dest.write( command );
                    break;

                case kCommandSET1:
                case kCommandPUT1:
                case kCommandRIGHT1:
                case kCommandW1:
                case kCommandX1:
                case kCommandDOWN1:
                case kCommandY1:
                case kCommandZ1:
                    dest.write( command );
                    dest.write( source, 1 );
                    break;

                case kCommandRIGHT2:
                case kCommandW2:
                case kCommandX2:
                case kCommandDOWN2: 
                case kCommandY2:
                case kCommandZ2:
                    dest.write( command );
                    dest.write( source, 2 );
                    break;

                case kCommandRIGHT3:
                case kCommandW3:
                case kCommandX3:
                case kCommandDOWN3:
                case kCommandY3:
                case kCommandZ3:
                    dest.write( command );
                    dest.write( source, 3 );
                    break;

                case kCommandRIGHT4:
                case kCommandW4:
                case kCommandX4:
                case kCommandDOWN4:
                case kCommandY4:
                case kCommandZ4:
                    dest.write( command );
                    dest.write( source, 4 );
                    break;

                case kCommandSETRULE:
                case kCommandPUTRULE:
                    dest.write( command );
                    dest.write( source, 8 );
                    break;

                case kCommandXXX1:
                case kCommandXXX2:
                case kCommandXXX3:
                case kCommandXXX4:
                    length = command - kCommandXXX1 + 1;
                    writeSpecial( source.string( source.unsigned( length )), dest, pageSpecialMap );
                    break;

                case kCommandFNT1:
                case kCommandFNT2:
                case kCommandFNT3:
                case kCommandFNT4:
                    length = command - kCommandFNT1 + 1;
                    writeFontSelect( source.unsigned( length ), dest, font, usedFont );
                    break;

                case kCommandFNTDEF1:
                case kCommandFNTDEF2:
                case kCommandFNTDEF3:
                case kCommandFNTDEF4:
                    length = command - kCommandFNTDEF1 + 1;
                    writeFontDefinition( source.unsigned( length ), source, font );
                    break;
                
                default:
                    throw new DVIFormatException(
                        "Unexpected DVI Command " + command );
            }
        }
    }

    final private static String kTranslatePrefix = "html:<a href=";

    private void writeSpecial( String special, DVIOutputStream dest, Hashtable pageSpecialMap )
            throws IOException {

        String translated = ( String ) pageSpecialMap.get( special );

        if( translated == null )
            translated = ( String ) specialMap.get( special );

        if( translated == null && translate != null &&
                special.regionMatches( true, 0, kTranslatePrefix, 0, kTranslatePrefix.length( ))) {

            int translateStart = kTranslatePrefix.length( );
            if( special.charAt( translateStart ) == '"' )
                translateStart ++;
            
            int translateEnd = translateStart;
            String element = null;
            Enumeration keys = translate.keys( );
            Enumeration elements = translate.elements( );

            while( element == null && keys.hasMoreElements( )) {
                String key = ( String ) keys.nextElement( );
                String nextElement = ( String ) elements.nextElement( );
                if( special.regionMatches( true, translateStart, key, 0, key.length( ))) {
                    translateEnd = translateStart + key.length( );
                    element = nextElement;
                }
            }

            if( element != null )
                translated =
                    special.substring( 0, translateStart ) +
                    element +
                    special.substring( translateEnd );
        }

        if( translated == null )
            translated = special;

        dest.writeVariableSized( kCommandXXX1, translated.length( ));
        dest.write( translated );
    }

    // This is a little bit misnamed -- it processes a font definition
    // during the write page phase, but doesn't actually *write* anything.
    // Instead, the font definition is written in writeFontSelect once it
    // is seen to be neccessary.

    private void writeFontDefinition( int number, DVIInputStream source, Hashtable font )
            throws IOException {
        
        byte[ ] parameters = new byte[ kFontHeaderLength ];
        source.read( parameters );

        int nameLength =
            parameters[ kFontHeaderLength - 2 ] +
            parameters[ kFontHeaderLength - 1 ];

        byte[ ] fontDef = new byte[ kFontHeaderLength + nameLength ];
        System.arraycopy( parameters, 0, fontDef, 0, kFontHeaderLength );
        source.read( fontDef, kFontHeaderLength, nameLength );

        font.put( new Integer( number ), fontDef );
    }

    private void writeFontSelect( int number, DVIOutputStream dest, Hashtable font, Hashtable usedFont )
            throws IOException {

        Integer key = new Integer( number );
        if( usedFont.get( key ) == null ) {
            byte[ ] fontDef = ( byte[ ] ) font.get( key );
            usedFont.put( key, fontDef );
            dest.writeVariableSized( kCommandFNTDEF1, number );
            dest.write( fontDef );
        }

        if( kLowFont + number <= kHighFont )
            dest.write( kLowFont + number );
        else
            dest.writeVariableSized( kCommandFNT1, number );
    }




    // File helper functions:

    private InputStream openDVIInputStream( ) throws IOException {
        try {
            return new URL( documentName ).openStream( );
        } catch( MalformedURLException e ) {
            return new BufferedInputStream( new FileInputStream( documentName ));
        }
    }

    private OutputStream openDVIOutputStream( int page ) throws IOException {
        context.showMessage( "Writing page " + page );

        String pageName = getDVIName( page );
        return new BufferedOutputStream( new FileOutputStream( pageName ));
    }

    private PrintStream openHTMLPrintStream( int page, int scale ) throws IOException {
        context.showMessage( "HTML scale " + scale + " page " + page );
        return openPrintStream( getHTMLName( page, scale ));
    }

    private PrintStream openPrintStream( String filename ) throws IOException {
        return new PrintStream( new BufferedOutputStream( new FileOutputStream( filename )));
    }

    private String getDVIName( int page ) {
        return pagePrefix + page + ".dvi";
    }

    private String getHTMLName( int page, int scale ) {
        return page == pageDefault && scale == scaleDefault
            ? index
            : pagePrefix + page + scalePrefix + scale + ".html";
    }
}
